T:Type, L:T List, f:(||L||T). (i:||L||. f(i) = L[i])  L = map(f;upto(||L||)) 

latex

Definitions	t  T, #$n, x:A. B(x), ||as||, n+m, {i..j}, Type, x:AB(x), car.cdr, {x:A| B(x) }, ij, P  Q, l[i], f(a), s = t, Prop, type List, nil, False, A, P & Q, AB, i  j < k, , a<b, x:AB(x), Void, x.A(x), P  Q, P  Q, n-m, True, T, , s ~ t, x:A. B(x), Top, upto(n), i=j, hd(l), i<j, ij, S  T, f o g
Lemmas	map-map, top wf, map append sq, upto wf, upto decomp, select cons tl, squash wf, le wf, length wf2, select wf, length cons, non neg length, int seg wf, length wf1